The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
colorof, !EQ, eqColorList, revapp, possible, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
!EQ < colorof
colorof < possible
eqColorList < colorrestthetrick
possible < colornode

(6) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

The following defined symbols remain to be analysed:
!EQ, colorof, eqColorList, revapp, possible, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
!EQ < colorof
colorof < possible
eqColorList < colorrestthetrick
possible < colornode

(7) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol !EQ.

(8) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

The following defined symbols remain to be analysed:
colorof, eqColorList, revapp, possible, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
colorof < possible
eqColorList < colorrestthetrick
possible < colornode

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol colorof.

(10) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

The following defined symbols remain to be analysed:
eqColorList, revapp, possible, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
eqColorList < colorrestthetrick
possible < colornode

(11) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

Induction Base:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, 0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) →_R^Ω(1)
False

Induction Step:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, +(n41_0, 1))), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(n41_0, 1))) →_R^Ω(1)
and(True, eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0))) →_IH
and(True, False) →_R^Ω(0)
False

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(12) Complex Obligation (BEST)

(13) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

The following defined symbols remain to be analysed:
revapp, possible, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
possible < colornode

(14) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
revapp(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4056454_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b)) → gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(n4056454_0, b)), rt ∈ Ω(1 + n4056454₀)

Induction Base:
revapp(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b)) →_R^Ω(1)
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b)

Induction Step:
revapp(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(n4056454_0, 1)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b)) →_R^Ω(1)
revapp(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4056454_0), Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b))) →_IH
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(+(b, 1), c4056455_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(15) Complex Obligation (BEST)

(16) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4056454_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b)) → gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(n4056454_0, b)), rt ∈ Ω(1 + n4056454₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

The following defined symbols remain to be analysed:
possible, colornode, colorrestthetrick

They will be analysed ascendingly in the following order:
possible < colornode

(17) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4058397_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) → True, rt ∈ Ω(1 + n4058397₀)

Induction Base:
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) →_R^Ω(1)
True

Induction Step:
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(n4058397_0, 1)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) →_R^Ω(1)
possible[Ite][True][Ite](eqColor(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), colorof(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0))), gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4058397_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) →_R^Ω(1)
possible[Ite][True][Ite](eqColor(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), NoColor), gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4058397_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) →_R^Ω(1)
possible[Ite][True][Ite](False, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4058397_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) →_R^Ω(0)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4058397_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) →_IH
True

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(18) Complex Obligation (BEST)

(19) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4056454_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b)) → gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(n4056454_0, b)), rt ∈ Ω(1 + n4056454₀)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4058397_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) → True, rt ∈ Ω(1 + n4058397₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

The following defined symbols remain to be analysed:
colornode, colorrestthetrick

(20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol colornode.

(21) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4056454_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b)) → gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(n4056454_0, b)), rt ∈ Ω(1 + n4056454₀)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4058397_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) → True, rt ∈ Ω(1 + n4058397₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

The following defined symbols remain to be analysed:
colorrestthetrick

(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol colorrestthetrick.

(23) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4056454_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b)) → gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(n4056454_0, b)), rt ∈ Ω(1 + n4056454₀)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4058397_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) → True, rt ∈ Ω(1 + n4058397₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

No more defined symbols left to analyse.

(24) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

(25) BOUNDS(n^1, INF)

(26) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4056454_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b)) → gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(n4056454_0, b)), rt ∈ Ω(1 + n4056454₀)
possible(gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4058397_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0)) → True, rt ∈ Ω(1 + n4058397₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

(28) BOUNDS(n^1, INF)

(29) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)
revapp(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n4056454_0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(b)) → gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(n4056454_0, b)), rt ∈ Ω(1 + n4056454₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

(31) BOUNDS(n^1, INF)

(32) Obligation:

Innermost TRS:
Rules:
colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
isPossible(CN(cl, n)) → True
isPossible(NotPossible) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) → colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) → colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, cs1, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Types:
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorof[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
and :: False:True → False:True → False:True
False :: False:True
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
possible[Ite][True][Ite] :: False:True → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colornode[Ite][True][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] → False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick[Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite]
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let][Ite] :: False:True → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → Cons:Nil:colorrest[Ite][True][Let][Ite] → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' → Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'1_0 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]2_0 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_False:True3_0 :: False:True
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0 :: Nat → N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0 :: Nat → Cons:Nil:colorrest[Ite][True][Let][Ite]

Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(0) ⇔ Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(+(x, 1)) ⇔ CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'4_0(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(0) ⇔ Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(x, 1)) ⇔ Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(+(1, n41_0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]5_0(n41_0)) → False, rt ∈ Ω(1 + n41₀)

(34) BOUNDS(n^1, INF)